b:, T:Type, A, B:(T List), x:T.
(x  if b then A else B fi )  (((b) & (x  A))  (((b)) & (x  B))) 

latex

Definitions	x:A. B(x), P  Q, if b then t else f fi , P  Q, P & Q, b, A, t  T, P  Q, tt, P  Q, True, , ff, {T}, , Unit, False,
Lemmas	bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot